(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v12 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const _4-0 (_ BitVec 4))
(declare-const v17 Bool)
(declare-const v19 Bool)
(assert (or v19 v17 v17 (and v4 v4 (= (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) (or v15 v7 v9 (= (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) v7 v12 v2 v6 v14 v9 v2) (= (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) (= (bvcomp (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) (bvcomp (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0))) (=> v6 (or v15 v7 v9 (= (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) v7 v12 v2 v6 v14 v9 v2)) v15 v8 (=> v6 (or v15 v7 v9 (= (bvurem (bvsmod _4-0 _4-0) (bvsmod _4-0 _4-0)) (bvsmod _4-0 _4-0)) v7 v12 v2 v6 v14 v9 v2)) v10)))
(check-sat)
